/*
 * cubelist.cpp
 *
 *  Created on: Mar 20, 2012
 *      Author: soselar
 */

#include "cubelist.h"

/*
cubelist::cubelist(fstream* input)
{
	string temp;
	*input >> temp;

	*input >> icount;
	cout << icount << endl;
//	cin >> ".o " >> "1" >> endl;
	*input >> temp;
	*input >> temp;

//	cin >> temp >> " 1" >> endl;

	*input >> temp;

	while (temp[0] != '.'){
		cube new_cube(temp, icount);
		cout << temp << endl;
		new_cube.valid = 1;
		cover.push_back(new_cube);
		*input >> temp;
		*input >> temp;
//		cin >> temp >> "1" >> endl;
	}

//	cout << "finish reading" << endl;
	for (int i = 0; i< icount; i++)
		index.push_back(i);
}
*/
/*
cubelist & cubelist::operator = (const cubelist &rhs)
{
	cover = rhs.cover;
	icount = rhs.icount;
	index = rhs.index;

	tree_index = rhs.tree_index;
	tree_v = rhs.tree_v;

	return *this;
}

cubelist& cubelist::operator += (const cubelist & a)
{
	index = a.index;

	for (int i = 0; i < a.cover.size(); i++)
		cover.push_back(a.cover[i]);

	return *this;
}

void cubelist::output(fstream* out)
{
	for (int i = 0; i < cover.size(); i++)
		*out << cover[i].output() << endl;
	*out << ".e" << endl;
	cout << ".e" << endl;
}
*/

void cubelist::output(FILE* out)
{
	char temp[50];
	int i, j;

	fprintf(out, ".i %d\n", icount);
	fprintf(out, ".o 1\n");

	for (i = 0; i < cover.size(); i++){
		for (j = 0; j < icount; j++){
			if (cover[i].element[j] == 1)
				temp[j] = '1';
			else if (cover[i].element[j] == 0)
				temp[j] = '0';
			else if (cover[i].element[j] == 2)
				temp[j] = '-';
		}
		temp[j] = '\0';
		fprintf(out, "%s 1\n", temp);
	}

	fprintf(out, ".e\n");
}

void cubelist::print_tree()
{
	int i;

	for (i = 0; i < tree_v.size(); i++){
		if (tree_v[i] == 0)
			cout << "x" << tree_index[i] << "' ";
		else
			cout << "x" << tree_index[i] << " ";
	}
}

bool cubelist::compare_cube(cube a, cube b)
{
	for (int i = 0; i< icount; i++)
		if (a.element[i] < b.element[i])
			return true;
		else if (a.element[i] > b.element[i])
			return false;

	return true;
}

int cubelist::split_var()
{
	int count[icount];
	int count_diff[icount];
	int binate[icount];
	int max_count;
	int min_diff;
	int i, j, flag;

	for (i = 0; i < icount; i++){
		count[i] = 0;
		count_diff[i] = 0;
		binate[i] = 0;
	}

	for (j = 0; j < cover.size(); j++)
		for (i = 0; i < icount; i++)
			if (cover[j].element[i] == 0){
				count[i]++;
				count_diff[i]--;
				if (binate[i] == 0)
					binate[i] = 1;
				else if (binate[i] == 2)
					binate[i] = 3;
			}
			else if (cover[j].element[i] == 1){
				count[i]++;
				count_diff[i]++;
				if (binate[i] == 0)
					binate[i] = 2;
				else if (binate[i] == 1)
					binate[i] = 3;
			}

	max_count = 0;
	min_diff = 32767;
	flag = 0;

	for (i = 0; i < icount; i++){
		if (binate[i] == 3){
			if(count[i] > max_count){
				max_count = count[i];
				min_diff = abs(count_diff[i]);
			}
			else if(count[i] == max_count){
				if (min_diff > abs(count_diff[i]))
					min_diff = abs(count_diff[i]);
			}
			if (flag == 0)
				flag = 1;
		}
	}

	if (flag == 0){
		for (i = 0; i < icount; i++){
			if(count[i] > max_count){
				max_count = count[i];
				min_diff = abs(count_diff[i]);
			}
			else if(count[i] == max_count){
				if (min_diff > abs(count_diff[i]))
					min_diff = abs(count_diff[i]);
			}
		}
	}

//	cout << max_count << " split_var " << min_diff << endl;
	for (i = 0; i< icount; i++){
		if(count[i] == max_count && min_diff == abs(count_diff[i])){
//			cout << " split_var is " << index[i] << endl;
			return index[i];
		}
	}
	return 0;
}

void cubelist::time(int var, int flag)
{
	int i, j;

	i = 0;
	while (index[i] < var){
		i++;
	}

//	cout << "split index:" << index[i] << endl;

	index.insert(index.begin() + i, var);

	for (j = 0; j < cover.size(); j++){
		if (flag == 1) //var == 1
			cover[j].element.insert(cover[j].element.begin() + i, 1);
		else //var == 0
			cover[j].element.insert(cover[j].element.begin() + i, 0);
	}
	icount++;
}

void cubelist::prime()
{
	int state;

	if (unate()){ //U1
		scc();
		print_tree();
		cout << "Teminate at U1: Leaf" << endl;
	}
	else{
		state = test();
		if (state == 1){
			cube temp;
			temp.add(icount);
			cover.clear();
			cover.push_back(temp);
			print_tree();
			cout << "Teminate at B1: Leaf" << endl;
		}

		else if (state == 2){
			cube temp;
			temp.add(icount);
			cover.clear();
			cover.push_back(temp);
			print_tree();
			cout << "Teminate at B2: Leaf" << endl;
		}

		else if (state == 3){
			print_tree();
			cout << "Teminate at B3: Leaf" << endl;
		}

		else if (state == 4){
			print_tree();
			cout << "Teminate at B4: Leaf" << endl;
		}

		else{
			cubelist sub0;
			cubelist sub1;
			int var, i;

			sub0.cover = cover;
			sub0.index = index;
			sub0.tree_index = tree_index;
			sub0.tree_v = tree_v;
			sub0.icount = icount;

			sub1.cover = cover;
			sub1.index = index;
			sub1.tree_index = tree_index;
			sub1.tree_v = tree_v;
			sub1.icount = icount;

			var = split_var();

			sub0.split(var, 0);
			sub1.split(var, 1);

			sub0.tree_index.push_back(var);
			sub1.tree_index.push_back(var);

			sub0.tree_v.push_back(0);
			sub1.tree_v.push_back(1);

			print_tree();
			cout << "Split at variable x" << var << ": Node" << endl;

			sub0.prime();
			sub1.prime();

			sub0.time(var, 0);
			sub1.time(var, 1);

			cover.clear();
			sub1.consensus(sub0);
			cover = sub1.cover;
			for (i = 0; i < sub0.cover.size(); i++)
				cover.push_back(sub0.cover[i]);
			scc();
		}
	}
}

int cubelist::test()
{
	int i, j, n;
	int state;

	n = cover.size();
	cube universal(n);
	for (j = 0; j < cover.size(); j++){
//		for (i = 0; i < cover[j].element.size(); i++)
//			cout << cover[j].element[i] << " ";

		if (cover[j] == universal) //B1
			return 1;
	}

	if (b2()) //B2
		return 2;

	if (cover.size() == 0){ //B3
		return 3;
	}

	state = 0;
	for (j = 0; j < (cover.size() - 1); j++)
		if (!(cover[j] == cover[j + 1])){
			state = 1;
			return 0;
		}

	if (cover.size() == 1 || state == 0){ //B4
		return 4;
	}

	return 0;
}

bool cubelist::b2()
{
	int dash_number;
	int i, j, xindex;
	int find1, find0;

	cubelist temp;

	for (j = 0; j < cover.size(); j++){
		dash_number = 0;
		for (i = 0; i < icount; i++){
			if (cover[j].element[i] == 2)
				dash_number++;
			else
				xindex = i;

//			cout << cover[j].element.size() << dash_number << j << endl;
		}

		if (dash_number == (icount - 1)){
			temp.cover.push_back(cover[j]);
			temp.index.push_back(xindex);
		}
	}

	for (i = 0; i < temp.index.size(); i++){
		find0 = 0;
		find1 = 0;
		for (j = 0; j < temp.cover.size(); j++){
			if (temp.cover[j].element[temp.index[i]] == 0)
				find0 = 1;
			if (temp.cover[j].element[temp.index[i]] == 1)
				find1 = 1;
			}
		if (find0 && find1){ //B2
			return true;
		}
	}
	return false;
}

void cubelist::split(int var, int flag)
{
	int i, j;
	i = j = 0;

	while (index[i] < var)
		i++;

//	cout << "split:" << index[i] << endl;
	index.erase(index.begin() + i);

	while (j < cover.size()){
		if (cover[j].element[i] != flag && cover[j].element[i] != 2)
			cover.erase(cover.begin() + j);
		else{
			cover[j].element.erase(cover[j].element.begin() + i);
			j++;
		}
	}

	icount--;
}

int cubelist::containing(cube a, cube b)
{
	int flag = -1;

	for (int i = 0; i < a.element.size(); i++){
		if (a.element[i] != b.element[i]){
			if (a.element[i] != 2 && b.element[i] != 2)
				return -1;
			if (flag == -1 || flag == 3){
				if (a.element[i] == 2)
					flag = 0; // a potentially contains b
				else
					flag = 1; // b potentially contains a
			}
			else if (flag == 0){
				if (b.element[i] == 2)
					return -1;
			}
			else{
				if (a.element[i] == 2)
					return -1;
			}
		}
		else if (flag == -1)
			flag = 3;
	}
	if (flag == 3)
		return 0;
	return flag;
}

void cubelist::sort()
{
	int i, j;

	for (i = 0; i < cover.size() - 1; i++)
		for (j = i + 1; j < cover.size(); j++)
			if (!compare_cube(cover[i], cover[j]))
				cover[i].element.swap(cover[j].element);
}

void cubelist::scc()
{
	int i, j, flag, n;

	i = j =  0;

	while(i < cover.size()){
		while(j < cover.size()){
			if (i != j){
				flag = containing(cover[i], cover[j]);
				if (flag == -1){
					j++;
				}
				else if (flag == 0){
					cover.erase(cover.begin() + j);
				}
				else{
					cover.erase(cover.begin() + i);
					if (i == cover.size())
						break;
					j = i + 1;
				}
			}
			else
				j++;
		}
		i++;
		j = i + 1;
		n = 0;
	}
}

void cubelist::consensus(cubelist a)
{
	int i, j, k, n, m;
	int flag;

	m = cover.size();

	for (i = 0; i < m; i++){
		for (j = 0; j < a.cover.size(); j++){
			flag = 0;
			cube temp;
			for (k = 0; k < icount; k++){
				if (cover[i].element[k] == a.cover[j].element[k] || cover[i].element[k] == 2)
					temp.element.push_back(a.cover[j].element[k]);
				else if (a.cover[j].element[k] == 2)
					temp.element.push_back(cover[i].element[k]);
				else if (flag == 0){
					flag++;
					temp.element.push_back(2);
				}
				else{
					flag++;
					break;
				}
			}

			if (temp.element.size() == icount && flag == 1){
				cover.push_back(temp);
//				cout << icount << ":push " << endl;
/*				for (n = 0; n < temp.element.size(); n++)
					cout << cover[i].element[n] << " ";
				cout << "a" << endl;
				for (n = 0; n < temp.element.size(); n++)
					cout << a.cover[j].element[n] << " ";
				cout << "b" << endl;
				for (n = 0; n < temp.element.size(); n++)
					cout << temp.element[n] << " ";
				cout << endl;
//				cout << "push" << endl;
 */
			}
		}
	}
}

void cubelist::intersect_consensus(int a)
{
	int i, j;
	int flag;

	cube temp;

	temp = cover[a];
	cover.erase(cover.begin() + a);

	i = 0;
	while (i < cover.size()){
		flag = 0;
		for (j = 0; j < icount; j++){
			if (temp.element[j] != 2)
				cover[i].element[j] = temp.element[j];

			else if (cover[i].element[j] == 2 || cover[i].element[j] == temp.element[j]){
				cover[i].element[j] = 2;
				flag++;
			}
			if (flag >= 2){
				cover.erase(cover.begin() + i);
				break;
			}
		}
		if (flag < 2)
			i++;
	}
}

void cubelist::essential1()
{
	int i;

	i = 0;
	while (i < cover.size()){
		cubelist temp;
		temp.cover = cover;
		temp.icount = icount;
		temp.cofactor(i);
		if (temp.tautology()){
			cover.erase(cover.begin() + i);
		}
		else
			i++;
	}
}

void cubelist::essential2()
{
	int i;

	i = 0;
	while (i < cover.size()){
		cubelist temp;
		temp.cover = cover;
		temp.icount = icount;
		temp.intersect_consensus(i);
		if (temp.tautology()){
			cover.erase(cover.begin() + i);
		}
		else
			i++;
	}
}

bool cubelist::tautology()
{
	cube universal(icount);
	int i, j, c, d;
	int count0, count1;

	for (i = 0; i< cover.size(); i++) //B1
		if (cover[i] == universal)
			return true;

	for (j = 0; j < icount; j++){ //B2
		count0 = 0;
		count1 = 0;
		for (i = 0; i< cover.size(); i++)
			if (cover[i].element[j] == 0)
				count0++;
			else
				count1++;
		if (count0 == cover.size() || count1 == cover.size())
			return false;
	}

	cubelist temp;

	temp.cover = cover;
	temp.icount = icount;
	count0 = 0;
	count1 = 0;
	i = 0;
	for (j = 0; j < icount; j++){ //B3
		if (cover[i].element[j] == 2)
			count0++;
		else
			count1 = j;
	}
	if (count0 == (icount - 1)){
		for(i = 0; i < cover.size(); i++)
			temp.cover[i].element[count1] = 2;
		if (temp.cover[i] == universal)
			return true;
	}
	else if (count0 == icount)
		return true;

	if (icount == 0 || cover.size() == 0) //B4
		return false;

	if (unate()) //U1
		return false;

	d = 0;
	for (i = 0; i< cover.size(); i++){
		c = 0;
		for (j = 0; j < icount; j++){
			if (cover[i].element[j] == 2)
				c++;
		}
		d = d + 2 ^ c;
	}
	if (d < 2 ^ icount)
		return false;

	int var = split_var();
	cubelist temp0, temp1;
	for (i = 0; i< cover.size(); i++){
		if (cover[i].element[var] == 1)
			temp0.cover.push_back(cover[i]);
		else if (cover[i].element[var] == 0)
			temp1.cover.push_back(cover[i]);
		else{
			temp0.cover.push_back(cover[i]);
			temp1.cover.push_back(cover[i]);
		}
	}
	for (i = 0; i< cover.size(); i++){
		temp0.cover[i].element[var] = 2;
		temp1.cover[i].element[var] = 2;
	}
	if (temp0.tautology() && temp1.tautology())
		return true;
	else
		return false;
}

void cubelist::cofactor(int a)
{
	int i, j;
	int flag;

	cube temp;

	temp = cover[a];
	cover.erase(cover.begin() + a);

	i = 0;
	while (i < cover.size()){
		flag = 0;
		for (j = 0; j < icount; j++){
			if (cover[i].element[j] != 2 && cover[i].element[j] != temp.element[j] && temp.element[j] != 2){
				cover.erase(cover.begin() + i);
				flag = 1;
				break;
			}
		}
		if (flag == 0)
			i++;
	}

	j = 0;
	while (j < icount){
		if (temp.element[j] != 2){
			icount--;
			temp.element.erase(temp.element.begin() + j);
			for (i = 0; i< cover.size(); i++)
				cover[i].element.erase(cover[i].element.begin() + j);
		}
		else
			j++;
	}
}

bool cubelist::unate()
{
	int a, b, c, d;
	for(b = 0; b < icount; b++){
		for(a = c = d = 0; a < cover.size(); a++){
			if(cover[a].element[b] == 0)
				c++;
			if(cover[a].element[b] == 1)
				d++;
			if(c != 0 && d != 0)
				return false;
		}
	}
	return true;
}

